es:ES, e1, e2:E, P:({e:E| loc(e) = loc(e1)  Id & first(e) }Prop).
loc(e2) = loc(e1)  Id  e(e1,e2].P(e)  Prop 

latex

Definitions	P  Q, P & Q, t  T, P  Q, x:A. B(x), P  Q, ES, E, Prop, first(e), , b, A, loc(e), Id, False, (e <loc e'), x(s), e  e' , A & B, x:A. B(x), e(e1,e2].P(e)
Lemmas	es-locl wf, es-le wf, es-le-loc, es-loc-pred, Id wf, es-loc wf, not wf, assert wf, es-first wf, es-E wf, event system wf, es-locl-iff